| Model: | ftwc v.3 (MA) |
| Parameter(s) | N = 8, TIME_BOUND = 5 |
| Property: | TimeMax (exp-time) |
mcsta/modest mcsta ftwc.jani -E N=8,TIME_BOUND=5 --props TimeMax -O out.txt Minimal --unsafe --es -S Memory --no-partial-results
| Walltime: | 55.2552924156189s |
| Return code: | 0 |
| Note(s): | The tool result '936789768153243/500000000' is tagged as incorrect. The reference result is '14147539327715842970938081149439827556191855684986157225275420283904447111639173866985598067681880129145471955175837520484728674160947632314097414522215685810225289457464569207661091813307674297797143727174955440899483387407321681291184424506984992879012095530345285342024382474295791214853480384950324618438986141022393122221483515220059469437753580148566940023111369720706495584592910594485865392023065207484361584743733034472966492554451495384839780894386232463996592241438310525820998238718273578495918691672707401317176748184096327147856287264972471729588120240871838813879102585106207566691951399630379924021184728534349249967428450718614502037376678686402345692320311432491400624417178668317054297945120230434734671616812283656994600039357609515482255775387934878545716862747289920261364983342431626411334568200844878035785326549818269149287216092984331688654368905681236451815235937234883596128115298847189295790398147570144922809063167063962528551290722287316226930957361364621078617332124555611429900248705271716919382952114182769664485935394801970185448606996794475223351459359903585908150996048008741267160553266728914830252425526888638356128136225965167103122471272719550780556236642932222129696893467798030685193910202459950136951210238061689767579289643629303538542482870365261684890789158469324399903966074520435527400513184215701818535283932228822505417379643982708346744529249186030685601025189583144333201907054210070389572822374379524345297468243673733681004505816067531925822483031159282502142162128798124696802883448494004237017224443773454288483864754258272527830640/7089094486886152998759701300155500901998069494141378595082824220245193350841445442005921773373232468017404127046556816066172763832380898910759166783537122001803327415928789825044733438472368045971841355042333453313408686801655334985604705662488624072106433169111514928011691630773128060762623647992193034103190205909522064284047406323039604970403662201093284654054668452958183491297234244286068372763681370374726266308384622991328027205137693205600349183630125185371154573438258533712673412092877867700804884242902932346745349737176013215024325934627692482375927103941857100787490885917030247827459468997131837311668119854984798438962147706033548207098166939858066166831031219780220860594464147951283203961313594611332813759008724366176890429238998756081269324185116147876631957504095092112063260715169869160852842053825386369654224518690209505776178114050426878639030562327723451225362726314274693283245586900228586107330822034570017057331353785903279175727640306095100457629735940432349260334397741951039453474516789481757111542043748817172460259862875923592130952148356005729896464017339356784874328772912970518594071618611390735874646725183844220406819689970562199385068078117100272085488538668067127129148217908112211166685047613169246816871377941639068555593821218761881242401764378919825272403279105173337534011696735068919735562378509544701365166973746868641592503726967758543209499093761767328716973178924345448469760039826975572631209478350903760987830627909300587633645379160137966039250297375844157563695341953903748513131242807046379927336025645261638001926334008796169' (approx. 1995676.5076113513) which means a relative error of '0.06118074289054226' which is larger than the goal precision '0.001'. |
| Relative Error: | 0.06118074289054226 |
ftwc.jani:model: info: ftwc is an MA model.
ftwc.jani: info: Need at least 40 bytes per state.
ftwc.jani: info: Explored 10299 states for N=8, TIME_BOUND=5.
Peak memory usage: 59 MB
Analysis results for ftwc.jani
Experiment N=8, TIME_BOUND=5
+ State space exploration
Min. state size: 40 bytes
States: 10299
Transitions: 12635
Branches: 26983
Rate: 73043 states/s
Time: 0.1 s
+ Property TimeMax
Value: 1873579.536306486
Bounds: [1873579.536306486, infinity)
Time: 54.6 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.0 s
Min. prob. 1 states: 10299
Time for min. prob. 1 states: 0.0 s
+ Essential states
Iterations: 3
Essential states: 5206
Transitions: 7542
Branches: 21890
Time: 0.0 s
+ Value iteration
Final error: 9.9998873816987E-07
Iterations: 182126
Time: 54.5 s
Exported results to file "/out.txt".
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.